| Definitions | x:A  B(x), A c B, t  T,  , Type,  , False,  A, A  B,   x. t(x), nullset(p;S), FinProbSpace, f(a), measure(C) q, s C, x(s), P   Q, Outcome,  , x:A  B(x),  x:A. B(x), P & Q, p-open(p),  x:A. B(x), s = t, t.1, x.A(x), #$n, r < s,  , {x:A| B(x)} , a < b, Void, qeq(r;s),  b, P  Q, P Q, {i..j }, n+m, (r/s), r n, r * s, countable-p-union(i.A(i)), -n, True, x f y,  , <a, b>, <+>, , g set, goset, a < b, a <p b, a < b,  , T, SqStable(P), P  Q, left + right, S  T, i j < k, suptype(S; T), b,  , (i = j), Unit, s ~ t, {T}, SQType(T), x,y:A//B(x;y), E(n;F), Top, type List, ||as||, RandomVariable(p;n),  a j < b. E(j), r s, a b,  , A  B, if b then t else f fi , EquivRel(T;x,y.E(x;y)), tt, x,y. t(x;y),  , n - m, r + s, r - s, upto(n), map(f;as), imax-list(L), i  j ,  x:A.B(x) |
| Lemmas | length-map, length upto, imax-list wf, map wf, upto wf, qless transitivity 1 qorder, mon ident q, qadd preserves qless, qadd ac 1 q, qadd comm q, qadd inv assoc q, qinverse q, qmul ac 1 qrng, qmul-qdiv-cancel3, qmul over plus qrng, qmul over minus qrng, qmul one qrng, qadd wf, q-geometric-series, qmul comm qrng, exp unroll q, qsum wf, squash wf, true wf, prod sum l q, qle weakening lt qorder, qsum-qle, quotient wf, btrue wf, b-union wf, int nzero wf, expectation wf, expectation-imax-list, expectation-constant, length wf nat, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, assert of eq int, eq int wf, bool wf, bnot wf, not wf, int seg wf, member-countable-p-union, qmul-positive, sq stable from decidable, decidable qless, qexp-positive, countable-p-union wf, int-rational, qmul wf, qexp wf, qdiv wf, not functionality wrt iff, assert-qeq, assert wf, qeq wf2, false wf, le wf, nullset wf, finite-prob-space wf, pi1 wf, rationals wf, qless wf, int inc rationals, p-open wf, nat wf, p-outcome wf, p-open-member wf, p-measure-le wf |